\begin{tabbing}
$\forall$${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $x$:ecl(${\it ds}$; ${\it da}$), ${\it es}$:event\_system\{i:l\}, $i$:Id.
\\[0ex]($\forall$$x$:Id. subtype\_rel(es{-}vartype(${\it es}$; $i$; $x$); fpf{-}cap(${\it ds}$; id{-}deq; $x$; top)))
\\[0ex]$\Rightarrow$ \=($\forall$$e$:es{-}E(${\it es}$). \+
\\[0ex](loc($e$) = $i$) $\Rightarrow$ subtype\_rel(es{-}valtype(${\it es}$; $e$); ma{-}valtype(${\it da}$; es{-}kind(${\it es}$; $e$))))
\-\\[0ex]$\Rightarrow$ (\=ecl{-}es{-}halt(${\it es}$; $x$)\+
\\[0ex]$\in$ $\mathbb{N}\rightarrow$\{$e$:es{-}E(${\it es}$)$\mid$ loc($e$) = $i$\} $\rightarrow$\{$e_{2}$:es{-}E(${\it es}$)$\mid$ loc($e_{2}$) = $i$\} $\rightarrow$prop\{i:l\})
\-
\end{tabbing}